home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / replace_2.06.0 < prev    next >
Text File  |  1992-04-03  |  25KB  |  676 lines
  1. %%% REPLACEMENTS
  2. %%% version 2.04.3 (based on replace_19.4)
  3. %%%   no longer need to recompute largest clause length when doing replacement
  4. %%%   erased corresponding equation and pulled out form when simplifying 
  5. %%%     rewrite rule
  6. %%%   rewrote clause during replacement
  7. %%% version 2.04.6
  8. %%%   added fixed_priority
  9. %%%   removed rewriting from replacement
  10. %%% version 2.05.2
  11. %%%   added clause splitting to top_level_replacement
  12. %%% version 2.05.3
  13. %%%   added support for Quintus Prolog
  14. %%%   made replacement work with fixed_priority
  15. %%% version 2.05.5
  16. %%%   fixed bug which caused clauses to be asserted with uninstantiated size
  17. %%% version 2.06.0
  18. %%%   apply once_replace_rules only once per round
  19. %%%   added early check for unit conflict
  20. %%%
  21. %%% Replace a literal by the definitions.
  22. %%% A set of rules are provided by the user. The rules are stored with
  23. %%%     a list of 0s and 1s. A literal with 1 means that it is a
  24. %%%     distinguished literal and can be replaced by its definitions.
  25. %%% New instances are generated by replacements. An instance is also
  26. %%%     associated with a list of 0s and 1s. A 0 means that the literal
  27. %%%     is a substitutable literal and can be used to generate instances
  28. %%%     of replace rules.
  29. %%% The algorithm is described as follows. First we find a rule and
  30. %%%     all its distinguishded literals Ls. Matched Ls with substitutable
  31. %%%     literals at the same time to generate instances.
  32. %%%     Repeat all the rules.
  33. %%%     Do the process iteratively until no new instances are generated.
  34. %%% Many procedures are defined in the hyper module.
  35. %%%     
  36. %%% An instance is user supported if the literal is.
  37. %%% An instance is backward supported if it is all negative or if all
  38. %%%     substitutable literals for positive distinguished literals are
  39. %%%     backward supported and the nondistinguished literals are all
  40. %%%     negative.
  41. %%% An instance is forward supported if it is all positive or if all
  42. %%%     substitutable literals for negative distinguished literals are
  43. %%%     forward supported and the nondistinguished literals are all
  44. %%%     positive.
  45. %%%
  46. %%% Add an option which only takes ground literals to do replacements.
  47. %%%     The option is ground_substitution.
  48. %%% 
  49. %%% We throw away instances if the sliding priority is used.
  50. %%% 
  51. %%% We keep two lists of literals, one is lit_N which is a list of new 
  52. %%%     literals obtained in the latest round, and the other is lit_ST
  53. %%%     which is a list accumulated from the beginning but not including
  54. %%%     the latest round.
  55. %%%
  56. %%% A matched distinguished literal is not allowed to be more specific
  57. %%%    than the form at the time it was matched.
  58. %%%    For example:
  59. %%%        [p(X), q(X), t(X)], [1,1,0]
  60. %%%    Suppose p(X) is matched to p(s(Y)), then the nucleus becomes
  61. %%%        [p(s(Y)), q(s(Y)), t(s(Y))]
  62. %%%    Now if there is a literal not(q(s(a))), then we can't
  63. %%%    match q(s(Y)) with not(q(s(a))) since this makes the first literal
  64. %%%    more specific than the form at the time it was matched.
  65. %%%    (p(s(a)) is more specific than p(s(Y)))
  66. %%%
  67. %%%    To implement this, we keep a list of variables from electrons.
  68. %%%    Whenever a distinguished literal matches another literal, we
  69. %%%    check if the list can unify with a constant list. If not, than
  70. %%%    the no_specific rule is violated. If so, the matching is allowed
  71. %%%    and we update the variable list.
  72. %%%
  73. %%% Ground literals are matched first.
  74. %%%
  75. %%% Allow two sets of replace rules. Replacements are done iteratively 
  76. %%%    for the first set until no new instances can be generated. 
  77. %%%    Then replacements are done once for the second set of rules. 
  78. %%%    Then replacements are done iteratively for the first set until
  79. %%%    no new instances can be generated.
  80. %%%
  81. %%% Allow replace variables in the electrons by individual constants.
  82. %%%    So we check the variable list. If an element is a constant,
  83. %%%    delete it. If it is a variable, keep it. Otherwise, reject it.
  84. %%%    However, we don't allow a matched electron to be more specific.
  85. %%%
  86. %%% ground restriction. The nucleus is ground after instantiation,
  87. %%%    not that the electrons are ground.
  88. %%%
  89. %%% ground substitution. The matching eletrons are ground.
  90. %%%
  91. %%% Add context literals.
  92. %%%    Allow context literals matching non-ground electrons for
  93. %%%    ground substitution.
  94. %%%
  95. %%% ground restriction on distinguished literals after matching.
  96. %%%     An option is added to require that the distinguished literals
  97. %%%     (not including context literals) after matching are ground.
  98. %%%
  99.  
  100.      top_level_replace :- not(not(top_level_replace_fail)).
  101.  
  102.      top_level_replace_fail :-
  103.         replacement,
  104.         cputime(TT1),
  105.         not(not(top_level_replace_0)),
  106.     split_clauses,
  107.         cputime(TT2),
  108.         TT3 is TT2 - TT1,
  109.         write_line(5,'Top level replace(s): ',TT3),
  110.         !.
  111.      top_level_replace_fail.
  112.        
  113. %%% Find all literals from clauses.
  114. %%% Find all instances by replacements.
  115. %%% Do more until no instances are generated.
  116.      top_level_replace_0 :-
  117.     no_replace_once,
  118.     !,
  119.     const_list(Clist),
  120.     repeated_replacements_1(Clist),
  121.     abolish(lit_ST_G,5),
  122.     abolish(lit_ST_V,5),
  123.     abolish(lit_N_G,5),
  124.     abolish(lit_N_V,5).
  125.      top_level_replace_0 :-
  126.     not(replace_rule_2(_,_,_,_,_)),
  127.     !,
  128.     const_list(Clist),
  129.     repeated_replacements_1(Clist),
  130.     abolish(lit_ST_G,5),
  131.     abolish(lit_ST_V,5),
  132.     abolish(lit_N_G,5),
  133.     abolish(lit_N_V,5).
  134.      top_level_replace_0 :-
  135.     const_list(Clist),
  136.     repeated_replacements_1(Clist),
  137.     once_replacements(Clist),
  138.     repeated_replacements_2(Clist),
  139.     abolish(lit_ST_G,5),
  140.     abolish(lit_ST_V,5),
  141.     abolish(lit_N_G,5),
  142.     abolish(lit_N_V,5).
  143.  
  144.      repeated_replacements_1(Clist) :-
  145.         not(not(rpl_lits(0,Clist))),
  146.     not(not(rpl_instances_call(repeated,Clist))).
  147.  
  148.      rpl_instances_call(Type,Clist) :-
  149.         not(not(rpl_instances(Type,Clist))),
  150.     not(not(litN_to_litST)),
  151.         not(not(rpl_lits(1,Clist))),
  152.     physically_erase(sent_C),
  153.         not(not(update_sentC_1(Clist))),
  154.         sentHM_to_sentC_a,
  155.         not(not(rpl_more(Type,Clist))), !.
  156.  
  157.      once_replacements(Clist) :-
  158.     not(not(litN_to_litST)),
  159.     not(not(rpl_instances_call(once,Clist))).
  160.  
  161.      repeated_replacements_2(Clist) :-
  162.     not(not(rpl_more(repeated,Clist))).
  163.  
  164. %%% Find a replace rule.
  165.      rpl_instances(repeated,Clist) :-
  166.         replace_rule_1(Rule,V1,W1,Flags,Contexts),
  167.         rpl_instances_rule(repeated,Rule,V1,W1,Flags,Contexts,Clist),
  168.     check_hm_stop, !.
  169.      rpl_instances(once,Clist) :-
  170.         replace_rule_2(Rule,V1,W1,Flags,Contexts),
  171.         rpl_instances_rule(once,Rule,V1,W1,Flags,Contexts,Clist),
  172.     check_hm_stop, !.
  173.      rpl_instances(_,_).
  174.        
  175. %%% Find all the instance of a replace rule.
  176. %%% We do unit deletion for instances.
  177. %%% A list of 0s and 1s are associated with an instance. The literal with
  178. %%%     1 would be deleted by unit deletion.
  179.      rpl_instances_rule(Type,Rule,V1,W1,Flags,Contexts,Clist) :-
  180.         print_rpl_rule(Rule,V1,Flags,Contexts),
  181.         rpl_sep_clause(Flags,Rule,Contexts,W1,Dg,NDg,DConts,Dw,VRule,VDg,VNDg),
  182.     negate_clause(Dg,NegDg),
  183.         !,
  184.         rpl_inst_rule(Type,Flags,Contexts,Rule,W1,NegDg,NDg,DConts,Dw,
  185.         VRule,VDg,VNDg,Clist).
  186.  
  187. %%% Initialize support and distance information.
  188. %%% Match distinguished literals.
  189. %%% Adjust user distance.
  190. %%% Miscellaneous things.
  191.      rpl_inst_rule(Type,Flags,Contexts,Rule,W1,NegDg,NDg,DConts,Dw,
  192.         VRule,VDg,VNDg,Clist) :-
  193.         rpl_rule_SR(Rule,DS1,DR1),
  194.         rpl_match_dgs(Type,NegDg,DConts,Dw,VDg,DS1,DR1,Clist,VL,DS2,DR2),
  195.     check_ground_disting_after_match(DConts,VDg,NegDg),
  196.         rpl_inst_rule_0(Flags,Contexts,Rule,W1,DS2,DR2,NDg,VRule,VNDg).
  197.  
  198. %%% If ground_disting_after_match is specified.
  199.      check_ground_disting_after_match(DConts,VDg,NegDg) :-
  200.     ground_disting_after_match,
  201.     union_lists(DConts,VDg,YY),
  202.         literals_remain_1(YY,NegDg,XX,_),
  203.     !, numbervars(XX,0,0), !.
  204.      check_ground_disting_after_match(_,_,_) :- !.
  205.     
  206. %%% Initialize support and distance information.
  207.      rpl_rule_SR(X,sp(0,1,1),ds(1,0,1)) :- negclause(X), !.
  208.      rpl_rule_SR(X,sp(0,1,1),ds(1,1,0)) :- posclause(X), !.
  209.      rpl_rule_SR(_,sp(0,1,1),ds(1,1,1)) :- !.
  210.  
  211.      rpl_match_dgs(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],
  212.         DS1,DR1,Clist,VL1,DS2,DR2) :-
  213.         rpl_match_dg_N(Type,D,DC,W,Dw,VD,DS1,DR1,Clist,VL1,Dw1,DSM,DRM,VLM),
  214.         rpl_match_dgs_R(Ds,DCs,Dw1,VDs,DSM,DRM,Clist,VLM,DS2,DR2).
  215.      rpl_match_dgs(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],
  216.         DS1,DR1,Clist,VL1,DS2,DR2) :-
  217.         rpl_match_dgs_1(Type,Ds,DCs,Dw,VDs,DS1,DR1,Clist,[D|Kg1],[DC|KDC1],
  218.         [W|Kw1],[VD|VKg1],Kg1,KDC1,Kw1,VKg1,VL1,DS2,DR2).
  219.      rpl_match_dgs_1(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],DS1,DR1,Clist,
  220.         Kg1,KDC1,Kw1,VKg1,Ds,DCs,Dw,VDs,VL1,DS2,DR2) :-
  221.         rpl_match_dg_N(Type,D,DC,W,Kw1,VD,DS1,DR1,Clist,VL1,Kw2,DSM,DRM,VLM),
  222.         rpl_match_dgs_R(Kg1,KDC1,Kw2,VKg1,DSM,DRM,Clist,VLM,DS2,DR2).
  223.      rpl_match_dgs_1(Type,[D|Ds],[DC|DCs],[W|Dw],[VD|VDs],DS1,DR1,Clist,
  224.         Kg1,KDC1,Kw1,VKg1,[D|Kg2],[DC|KDC2],[W|Kw2],[VD|VKg2],
  225.         VL1,DS2,DR2) :-
  226.         rpl_match_dgs_1(Type,Ds,DCs,Dw,VDs,DS1,DR1,Clist,Kg1,KDC1,Kw1,VKg1,
  227.         Kg2,KDC2,Kw2,VKg2,VL1,DS2,DR2).
  228.  
  229. %%% If the distinguished literal is ground, then no backtracking.
  230.      rpl_match_dg_N(Type,D,DC,W,Dw1,VD,DS1,DR1,Clist,VL1,Dw1,DS2,DR2,VL2) :-
  231.     var(W),
  232.         !,
  233.     rpl_match_new_literal(Type,VD,D,DC,Wn1,LS1,LR1),
  234.     check_electron_vars(Wn1,Wn2),
  235.     expand_VL(Wn2,VL1,VL2),
  236.         onematch_SR(D,DS1,DR1,LS1,LR1,DS2,DR2), !.
  237.      rpl_match_dg_N(Type,D,DC,_,Dw1,VD,DS1,DR1,Clist,VL1,Dw2,DS2,DR2,VL2) :-
  238.     rpl_match_new_literal(Type,VD,D,DC,Wn1,LS1,LR1),
  239.     check_electron_vars(Wn1,Wn2),
  240.     check_electron_vars(VL1,VLM),
  241.     not(not(VLM = Clist)),
  242.     w1_w2(Dw1,Dw2),
  243.     expand_VL(Wn2,VLM,VL2),
  244.         onematch_SR(D,DS1,DR1,LS1,LR1,DS2,DR2).
  245.  
  246. %%% If no ground_substitution, then take all.
  247. %%% If ground_substitution and context literal, take all.
  248. %%% Otherwise, stop.
  249.      rpl_match_new_literal(repeated,VD,D,_,Wn1,LS1,LR1) :-
  250.         lit_N_G(VD,D,Wn1,LS1,LR1).
  251.      rpl_match_new_literal(repeated,VD,D,_,Wn1,LS1,LR1) :-
  252.     \+ ground_substitution,
  253.     !, lit_N_V(VD1,D1,Wn1,LS1,LR1),
  254.         unify(VD,VD1),
  255.         unify(D,D1).
  256.      rpl_match_new_literal(repeated,VD,D,1,Wn1,LS1,LR1) :-
  257.     lit_N_V(VD1,D1,Wn1,LS1,LR1),
  258.         unify(VD,VD1),
  259.         unify(D,D1).
  260.      rpl_match_new_literal(once,VD,D,_,Wn1,LS1,LR1) :-
  261.         lit_ST_G(VD,D,Wn1,LS1,LR1).
  262.      rpl_match_new_literal(once,VD,D,_,Wn1,LS1,LR1) :-
  263.     \+ ground_substitution,
  264.         !, lit_ST_V(VD1,D1,Wn1,LS1,LR1),
  265.         unify(VD,VD1),
  266.         unify(D,D1).
  267.      rpl_match_new_literal(once,VD1,D1,1,Wn1,LS1,LR1) :-
  268.         lit_ST_V(VD,D,Wn1,LS1,LR1),
  269.         unify(VD,VD1),
  270.         unify(D,D1).
  271.  
  272. %%% If an element is an individual constant, delete it.
  273. %%% If an element is a variable, keep it.
  274. %%% Otherwise, reject it.
  275.      check_electron_vars(VL2,VL2) :-
  276.     var(VL2), !.
  277.      check_electron_vars([X|Xs],VL2) :-
  278.     atomic(X),
  279.     !, check_electron_vars(Xs,VL2).
  280.      check_electron_vars([X|Xs],[X|VL2]) :-
  281.     var(X),
  282.     !, check_electron_vars(Xs,VL2).
  283.      check_electron_vars(_,_) :-
  284.     !, fail.
  285.  
  286. %%% Match one distinguished literal against lit_N or lit_ST.
  287.      rpl_match_dg_A(0,L1,DC1,T1,DS1,DR1,Clist,VL1,DS2,DR2,VL2) :-
  288.         rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1),
  289.     check_electron_vars(Wn1,Wn2),
  290.     expand_VL(Wn2,VL1,VL2),
  291.         onematch_SR(L1,DS1,DR1,LS1,LR1,DS2,DR2), !.
  292.      rpl_match_dg_A(1,L1,DC1,T1,DS1,DR1,Clist,VL1,DS2,DR2,VL2) :-
  293.         rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1),
  294.     check_electron_vars(Wn1,Wn2),
  295.     check_electron_vars(VL1,VLM),
  296.     not(not(VLM = Clist)),
  297.     expand_VL(Wn2,VLM,VL2),
  298.         onematch_SR(L1,DS1,DR1,LS1,LR1,DS2,DR2).
  299.  
  300. %%% If no ground_substitution, then take all.
  301. %%% If ground_substitution and context literal, take all.
  302. %%% Otherwise, stop.
  303.      rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1) :-
  304.     rpl_match_N_ST_1(T1,L1,DC1,Wn1,LS1,LR1).
  305.      rpl_match_N_ST(T1,L1,DC1,Wn1,LS1,LR1) :-
  306.     rpl_match_N_ST_2(T1,L1,DC1,Wn1,LS1,LR1).
  307.  
  308.      rpl_match_N_ST_1(T1,L1,_,Wn1,LS1,LR1) :-
  309.         lit_ST_G(T1,L1,Wn1,LS1,LR1).
  310.      rpl_match_N_ST_1(T1,L1,_,Wn1,LS1,LR1) :-
  311.     \+ ground_substitution,
  312.     !, lit_ST_V(T1a,L1a,Wn1,LS1,LR1),
  313.         unify(T1,T1a),
  314.         unify(L1,L1a).
  315.      rpl_match_N_ST_1(T1,L1,1,Wn1,LS1,LR1) :-
  316.     lit_ST_V(T1a,L1a,Wn1,LS1,LR1),
  317.         unify(T1,T1a),
  318.         unify(L1,L1a).
  319.  
  320.      rpl_match_N_ST_2(T1,L1,_,Wn1,LS1,LR1) :-
  321.         lit_N_G(T1,L1,Wn1,LS1,LR1).
  322.      rpl_match_N_ST_2(T1,L1,_,Wn1,LS1,LR1) :-
  323.     \+ ground_substitution,
  324.         !, lit_N_V(T1a,L1a,Wn1,LS1,LR1),
  325.         unify(T1,T1a),
  326.         unify(L1,L1a).
  327.      rpl_match_N_ST_2(T1,L1,1,Wn1,LS1,LR1) :-
  328.         lit_N_V(T1a,L1a,Wn1,LS1,LR1),
  329.         unify(T1,T1a),
  330.         unify(L1,L1a).
  331.  
  332. %%% Match the rest distinguished literals against lit_ST and lit_N.
  333.      rpl_match_dgs_R([L|Ls],DCs,Ws,Ts,DS1,DR1,Clist,VL1,DS2,DR2) :-
  334.     rpl_lit_reorder_4(Ws,[L|Ls],DCs,Ts,W1,Ws1,L1,Ls1,DC1,DCs1,T1,Ts1),
  335.         !, rpl_match_dg_A(0,L1,DC1,T1,DS1,DR1,Clist,VL1,DSM,DRM,VLM),
  336.         !, rpl_match_dgs_R(Ls1,DCs1,Ws1,Ts1,DSM,DRM,Clist,VLM,DS2,DR2).
  337.      rpl_match_dgs_R([L1|Ls1],[DC1|DCs1],[_|Ws1],[T1|Ts1],
  338.         DS1,DR1,Clist,VL1,DS2,DR2) :-
  339.         rpl_match_dg_A(1,L1,DC1,T1,DS1,DR1,Clist,VL1,DSM,DRM,VLM),
  340.     w1_w2(Ws1,Ws2),
  341.         rpl_match_dgs_R(Ls1,DCs1,Ws2,Ts1,DSM,DRM,Clist,VLM,DS2,DR2).
  342.      rpl_match_dgs_R([],[],[],[],DS2,DR2,_,_,DS2,DR2).
  343.     
  344. %%% Do unit simplification on undistinguished literals.
  345.      rpl_inst_rule_0(Flags,Contexts,Rule,W1,DS2,DR2,NDg,VRule,VNDg) :-
  346.     negate_clause(NDg,NegNDg),
  347.         rpl_unitsimp(NegNDg,VNDg,RNDg),
  348.     union_lists(VRule,Contexts,Dlist),
  349.         literals_remain_3(Dlist,Rule,W1,Flags,CnM,WM,FM,_),
  350.         rpl_inst_rule_1(CnM,WM,FM,DS2,DR2,RNDg), !.
  351.  
  352. %%% If the instance is a tautology, removes it.
  353. %%% Turn off tautology checking.
  354. %    rpl_inst_rule_1(C1,_,_,_,_,_) :-
  355. %       fol_tautology_clause(C1), !.
  356.      rpl_inst_rule_1(C1,W1,F1,DS1,DR1,RNDg) :-
  357.         delete_replicate_literals_3(C1,W1,F1,C2,W2,F2),
  358.     vars_W1_V1(W2,V2),
  359.         !,
  360.         check_numbervars(V2,'Number of variables overflows in instances !'),
  361.     !, check_ground_restriction(V2),
  362.         calculate_S(C2,RNDg,DS1,DS2),
  363.         calculate_priority_clause(C2,DS2,DR1,CP2),
  364.         rpl_processC(C2,V2,W2,F2,CP2,DS2,DR1), 
  365.     check_empty_hm(C2), !.
  366.  
  367.      check_ground_restriction(V1) :-
  368.         ground_restriction,
  369.         !,
  370.         var(V1).
  371.      check_ground_restriction(_).
  372.        
  373. %%% Unit simplification.
  374.      rpl_unitsimp([L1|Ls1],[0|Ls2],[L1|Ls3]) :-
  375.         \+ unit_instance(L1), !,
  376.         rpl_unitsimp(Ls1,Ls2,Ls3).
  377.      rpl_unitsimp([L1|Ls1],[1|Ls2],Ls3) :-
  378.         !,
  379.         rpl_unitsimp(Ls1,Ls2,Ls3).
  380.      rpl_unitsimp([],[],[]).
  381.        
  382. %%% Calculate support information.
  383. %%% Notice that RNDg is negated.
  384.      calculate_S(C1,_,sp(S11,_,_),sp(S11,1,0)) :-
  385.         negclause(C1), !.
  386.      calculate_S(C1,_,sp(S11,_,_),sp(S11,0,1)) :-
  387.         posclause(C1), !.
  388.      calculate_S(_,RNDg,sp(S11,S12,_),sp(S11,S12,0)) :-
  389.         posclause(RNDg), !.
  390.      calculate_S(_,RNDg,sp(S11,_,S13),sp(S11,0,S13)) :-
  391.         negclause(RNDg), !.
  392.      calculate_S(_,_,sp(S11,_,_),sp(S11,0,0)).
  393.          
  394.  
  395. %%% If no more instances were generated, done.
  396. %%% Otherwise, do more iterations.
  397.      rpl_more(once,_) :- !.
  398.      rpl_more(Type,_) :-
  399.     \+ new_literal_N, !.
  400.      rpl_more(Type,Clist) :-
  401.         repeat,
  402.         rpl_more_1(Type,Clist).
  403.  
  404.      rpl_more_1(_,_) :-
  405.     check_hm_stop, !.
  406.      rpl_more_1(Type,Clist) :-
  407.         not(not(rpl_instances(Type,Clist))),
  408.         not(not(litN_to_litST)),
  409.         not(not(rpl_lits(1,Clist))),
  410.     physically_erase(sent_C),
  411.     not(not(update_sentC_1(Clist))),
  412.         sentHM_to_sentC_a,
  413.     !,
  414.     \+ new_literal_N.
  415.  
  416.      new_literal_N :-
  417.         lit_N_G(_,_,_,_,_), !.
  418.      new_literal_N :-
  419.         lit_N_V(_,_,_,_,_), !.
  420.  
  421. %%% Move lit_N to lit_ST.
  422.      litN_to_litST :-
  423.     litN_to_litST_G,
  424.     litN_to_litST_V, !.
  425.  
  426.      litN_to_litST_G :-
  427.         retract(lit_N_G(A1,A2,A3,A4,A5)),
  428.         assertz(lit_ST_G(A1,A2,A3,A4,A5)),
  429.         fail.
  430.      litN_to_litST_G.
  431.        
  432.      litN_to_litST_V :-
  433.         retract(lit_N_V(A1,A2,A3,A4,A5)),
  434.         assertz(lit_ST_V(A1,A2,A3,A4,A5)),
  435.         fail.
  436.      litN_to_litST_V.
  437.        
  438. %%% Process the generated instance of the rule.
  439. %%%     Instances are treated as hyper-matches. Deletions may be done
  440. %%%     due to work-unit bound or priority bound.
  441. %%%
  442.      rpl_processC(Cn2,V2,W2,F2,CP2,CS1,CR1) :-
  443.     not(fixed_priority),
  444.     not(slidepriority),
  445.     !,
  446.         rpl_processC_1(Cn2,V2,W2,F2,CP2,CS1,CR1), !.
  447.      rpl_processC(Cn2,V2,W2,F2,CP2,CS1,CR1) :-
  448.          rpl_processC_2(Cn2,V2,W2,F2,CP2,CS1,CR1), !.
  449.  
  450.      rpl_processC_1(Cn2,V1,W1,F2,CP2,CS1,CR1) :-
  451.         clause_size(Cn2,CSize2),
  452.         rpl_proc_npr(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
  453.  
  454. %%% Consider priority.
  455.      rpl_processC_2(Cn2,V1,W1,F2,CP2,CS1,CR1) :-
  456.         priority_bound(PrioBound),
  457.         !,
  458.         check_prioritybound(CP2,PrioBound),
  459.         clause_size(Cn2,CSize2),
  460.         rpl_processC_3(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
  461.  
  462.      rpl_processC_3(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1) :-
  463.         fixed_priority,
  464.     !,
  465.         rpl_proc_npr(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
  466.      rpl_processC_3(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1) :-
  467.         slidepriority,
  468.     !,
  469.         rpl_proc_pr(CSize2,CP2,F2,Cn2,V1,W1,CS1,CR1).
  470.  
  471. %%% Find literals from clauses.
  472.      rpl_lits(Type,Clist) :-
  473.         rpl_sent(Type,Cn1,W1,CS1,CR1,Unit),
  474.         rpl_lits_clause(Cn1,W1,CS1,CR1,Unit,Clist),
  475.         fail.
  476.      rpl_lits(_,_).
  477.        
  478. %%% In first iteration, we take all literals from sent_C.
  479. %%% We don't count literals with 1.
  480.      rpl_sent(0,Cn1,W1,CS1,CR1,Unit) :-
  481.         clause(sent_C(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),true,
  482.         Cref),
  483.     not(logically_erased(sent_C,Cref)),
  484.         decide_unit(CnM,Unit),
  485.         literals_remain_2(F1,CnM,WM,Cn1,W1,_).
  486. %%% Otherwise, we take all literals from sent_HM.
  487. %%% We don't count literals with 1.
  488.      rpl_sent(1,Cn1,W1,CS1,CR1,Unit) :-
  489.         sent_HM(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),
  490.         decide_unit(CnM,Unit),
  491.         literals_remain_2(F1,CnM,WM,Cn1,W1,_).
  492.      rpl_sent(1,Cn1,W1,CS1,CR1,Unit) :-
  493.         sent_T(cl(_,_,by(CnM,V11,V11,_,WM),_,CS1,CR1,_,F1,_)),
  494.         decide_unit(CnM,Unit),
  495.         literals_remain_2(F1,CnM,WM,Cn1,W1,_).
  496.  
  497. %%% Check for duplicates.
  498. %%% Assert the literals.
  499.      rpl_lits_clause([Ln1|Lns1],[Wn1|Wns1],CS1,CR1,LU1,Clist) :-
  500.         \+ rpl_lit_copy(LU1,Ln1,Wn1,CS1,CR1,Clist),
  501.     assert_lit_N(LU1,Ln1,Wn1,CS1,CR1),
  502.         !,
  503.         rpl_lits_clause(Lns1,Wns1,CS1,CR1,LU1,Clist).
  504.      rpl_lits_clause([_|Lns1],[_|Wns1],CS1,CR1,LU1,Clist) :-
  505.         !,
  506.         rpl_lits_clause(Lns1,Wns1,CS1,CR1,LU1,Clist).
  507.      rpl_lits_clause([],[],_,_,_,_).
  508.        
  509.      assert_lit_N(LU1,Ln1,Wn1,CS1,CR1) :-
  510.     var(Wn1),
  511.         !, assertz(lit_N_G(LU1,Ln1,Wn1,CS1,CR1)), !.
  512.      assert_lit_N(LU1,Ln1,Wn1,CS1,CR1) :-
  513.         assertz(lit_N_V(LU1,Ln1,Wn1,CS1,CR1)), !.
  514.  
  515. %%% Check duplicates against lit_N first.
  516. %%% Check duplicates against lit_ST if necessary.
  517.      rpl_lit_copy(LU1,Ln1,Wn1,CS1,CR1,Clist) :-
  518.     var(Wn1),
  519.     !, rpl_lit_copy_G(LU1,Ln1,CS1,CR1).
  520.      rpl_lit_copy(LU1,Ln1,Clist,CS1,CR1,Clist) :-
  521.     rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist).
  522.  
  523.      rpl_lit_copy_G(LU1,Ln1,CS1,CR1) :-
  524.     lit_N_G(LU2,Ln1,_,CS2,CR2),
  525.     binary_max_ind(LU2,LU1,LU3,Up),
  526.     max_CS_ind(CS2,CS1,CS3,Up),
  527.     min_CR_ind(CR2,CR1,CR3,Up),
  528.     rpl_lit_copy_G_1(Up,0,LU3,CS3,CR3,Ln1), !.
  529.      rpl_lit_copy_G(LU1,Ln1,CS1,CR1) :-
  530.     lit_ST_G(LU2,Ln1,_,CS2,CR2),
  531.     binary_max_ind(LU2,LU1,LU3,Up),
  532.     max_CS_ind(CS2,CS1,CS3,Up),
  533.     min_CR_ind(CR2,CR1,CR3,Up),
  534.     rpl_lit_copy_G_1(Up,1,LU3,CS3,CR3,Ln1), !.
  535.  
  536.      rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist) :-
  537.         lit_N_V(LU2,Ln1,Clist,CS2,CR2),
  538.         binary_max_ind(LU2,LU1,LU3,Up),
  539.         max_CS_ind(CS2,CS1,CS3,Up),
  540.         min_CR_ind(CR2,CR1,CR3,Up),
  541.         rpl_lit_copy_V_1(Up,0,LU3,CS3,CR3,Ln1,Clist), !.
  542.      rpl_lit_copy_V(LU1,Ln1,CS1,CR1,Clist) :-
  543.         lit_ST_V(LU2,Ln1,Clist,CS2,CR2),
  544.         binary_max_ind(LU2,LU1,LU3,Up),
  545.         max_CS_ind(CS2,CS1,CS3,Up),
  546.         min_CR_ind(CR2,CR1,CR3,Up),
  547.         rpl_lit_copy_V_1(Up,1,LU3,CS3,CR3,Ln1,Clist), !.
  548.  
  549.      rpl_lit_copy_G_1(n,_,_,_,_,_) :- !.
  550.      rpl_lit_copy_G_1(_,0,LU3,CS3,CR3,Ln1) :-
  551.     retract(lit_N_G(_,Ln1,Wn1,_,_)),
  552.     assertz(lit_N_G(LU3,Ln1,Wn1,CS3,CR3)).
  553.      rpl_lit_copy_G_1(_,1,LU3,CS3,CR3,Ln1) :-
  554.     retract(lit_ST_G(_,Ln1,Wn1,_,_)),
  555.     assertz(lit_ST_G(LU3,Ln1,Wn1,CS3,CR3)).
  556.  
  557. %%% Update database for lit_N or lit_ST.
  558.      rpl_lit_copy_V_1(n,_,_,_,_,_,_) :- !.
  559.      rpl_lit_copy_V_1(_,0,LU3,CS3,CR3,Ln1,Clist) :-
  560.         clause(lit_N_V(_,Ln1,Clist,_,_),true,Ref2),
  561.         clause(lit_N_V(_,Ln2,Wn2,_,_),true,Ref2),
  562.         erase(Ref2),
  563.         assertz(lit_N_V(LU3,Ln2,Wn2,CS3,CR3)).
  564.      rpl_lit_copy_V_1(_,1,LU3,CS3,CR3,Ln1,Clist) :-
  565.         clause(lit_ST_V(_,Ln1,Clist,_,_),true,Ref2),
  566.         clause(lit_ST_V(_,Ln2,Wn2,_,_),true,Ref2),
  567.         erase(Ref2),
  568.         assertz(lit_ST_V(LU3,Ln2,Wn2,CS3,CR3)).
  569.  
  570. %%% Check for unit simplification.
  571.      unit_instance(L1) :-
  572.         numbervars(L1,0,_), !,
  573.         unit_instance_1(L1).
  574.  
  575.      unit_instance_1(L1) :-
  576.         clause(sent_C(cl(_,_,by([L1],V11,V11,_,_),_,_,_,_,_,_)),true,
  577.         Cref),
  578.     not(logically_erased(sent_C,Cref)).
  579.      unit_instance_1(L1) :-
  580.         sent_HM(cl(_,_,by([L1],V11,V11,_,_),_,_,_,_,_,_)).
  581.  
  582. %%% Check if the instance is a duplicate or if unit conflict. Assert it if it
  583. %%% is not.
  584.      rpl_proc_npr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
  585.         rpl_update_HM(CSize1,CP1,F1,Cn1,V1,CS1,CR1), !.
  586.      rpl_proc_npr(_,_,_,Cn1,_,_,_,_) :-
  587.     (check_unit_conflict_C(Cn1); check_unit_conflict_HM(Cn1)),
  588.     !,
  589.     assert_tryresult('unsatisfiable'),
  590.     assert_prooftype('UC').
  591.      rpl_proc_npr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
  592.         proc_C(0,_,Cn1,V1,W1,CN1,Cn2,V21,V22,V2,W2),
  593.         print_HM(Cn1,V1,CS1,CR1,F1),
  594.         asserta(sent_HM(cl(CSize1,CN1,by(Cn2,V21,V22,V2,W2),
  595.                 0,CS1,CR1,1,F1,CP1))), !.
  596.  
  597.      rpl_proc_pr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
  598.         rpl_update_HM(CSize1,CP1,F1,Cn1,V1,CS1,CR1), !.
  599.      rpl_proc_pr(_,_,_,Cn1,_,_,_,_) :-
  600.     (check_unit_conflict_C(Cn1); check_unit_conflict_HM(Cn1)),
  601.     !,
  602.     assert_tryresult('unsatisfiable'),
  603.     assert_prooftype('UC').
  604.      rpl_proc_pr(CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1) :-
  605.         prio_parameters(TotalHm,ExpectWU,TotalWU), !,
  606.         totalhm_test1(rpl,_,0,CSize1,CP1,F1,Cn1,V1,W1,CS1,CR1,
  607.                 TotalHm,ExpectWU,TotalWU), !.
  608.  
  609. %%% Check for duplicates.
  610.      rpl_update_HM(CSize1,CP1,F1,Cn1,V1,CS1,CR1) :-
  611.         const_list(V1),
  612.         rpl_update_HM(CSize1,CP1,F1,Cn1,CS1,CR1).
  613.  
  614. %%% Check for duplicates.
  615. %%% Against sent_HM, then sent_C.
  616.      rpl_update_HM(CSize1,CP1,F1,Cn1,CS1,CR1) :-
  617.         update_HM_1(CSize1,CP1,F1,Cn1,CS1,CR1).
  618.      rpl_update_HM(CSize1,CP1,F1,Cn1,CS1,CR1) :-
  619.     update_HM_2(CSize1,CP1,F1,Cn1,CS1,CR1).
  620.      rpl_update_HM(CSize1,CP1,F1,Cn1,CS1,CR1) :-
  621.         rpl_update_HM_2(CSize1,CP1,F1,Cn1,CS1,CR1).
  622.  
  623. %%% Against sent_C.
  624.      rpl_update_HM_2(CSize1,CP1,F1,Cn1,CS1,CR1) :-
  625.         clause(sent_C(cl(CSize1,CN1,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,
  626.         Cref),
  627.     not(logically_erased(sent_C,Cref)),
  628.         const_list(V2),
  629.         rpl_update_HM_21(CSize1,CN1,Cn1,CS1,CR1,F1,CP1).
  630.  
  631.      rpl_update_HM_21(CSize1,CN1,Cn1,CS1,CR1,F1,CP1) :-
  632.         clause(sent_C(cl(_,_,by(Cn1,V21,V21,V2,_),_,_,_,_,_,_)),true,Ref2),
  633.     not(logically_erased(sent_C,Ref2)),
  634.         const_list(V2),
  635.         clause(sent_C(cl(_,_,BY_2,_,_,_,_,_,_)),true,Ref2),
  636.         asserta(sent_T(cl(CSize1,CN1,BY_2,0,CS1,CR1,1,F1,CP1))).
  637.         
  638. %%% print replace rules and instances.
  639.      print_rpl_rule(C,V,F,X) :-
  640.         outinst,
  641.         write_line(5,'Current Replace Rule is :'),
  642.         print_clause_2(10,C,V),
  643.     tab(15), write(F), write(', '), write(X), nl,
  644.         write_line(5,'Instances are :'), !.
  645.      print_rpl_rule(_,_,_,_) :- !.
  646.        
  647. %%% Separate replace rule.
  648.      rpl_sep_clause([0|Flags],[R|Rule],[_|DC],[_|Ws],Dg,[R|NDg],DCs,Dw,
  649.                 [X|VRule],VDg,[X|VNDg]) :-
  650.         rpl_sep_clause(Flags,Rule,DC,Ws,Dg,NDg,DCs,Dw,VRule,VDg,VNDg).
  651.      rpl_sep_clause([1|Flags],[R|Rule],[DC|DCs],[W|Ws],[R|Dg],NDg,
  652.         [DC|DCs1],[W|Dw],[X|VRule],[X|VDg],VNDg) :-
  653.         rpl_sep_clause(Flags,Rule,DCs,Ws,Dg,NDg,DCs1,Dw,VRule,VDg,VNDg).
  654.      rpl_sep_clause([],[],[],[],[],[],[],[],[],[],[]).
  655.  
  656. %%% Expand variable list.
  657.      expand_VL(Wn1,VL1,VL1) :-
  658.     var(Wn1), !.
  659.      expand_VL([W|Wn1],VL1,VL2) :-
  660.     not_identical_in(W,VL1), !,
  661.     expand_VL(Wn1,[W|VL1],VL2).
  662.      expand_VL([W|Wn1],VL1,VL2) :-
  663.     expand_VL(Wn1,VL1,VL2).
  664.  
  665.      not_identical_in(W,VL1) :-
  666.     var(VL1), !.
  667.      not_identical_in(W,[V|VL1]) :-
  668.     W == V, !, fail.
  669.      not_identical_in(W,[_|VL1]) :-
  670.     !,
  671.     not_identical_in(W,VL1).
  672.  
  673.      rpl_lit_reorder_4(Ws,Ls,DCs,Ts,W1,Ws1,L1,Ls1,DC,DCs1,T1,Ts1) :-
  674.     replace_literal_reordering,
  675.     !, sep_gr_lit_4(Ws,Ls,DCs,Ts,W1,Ws1,L1,Ls1,DC,DCs1,T1,Ts1).
  676.